Memory management in L4

Mach has an intricate memory management system which allows the task to communicate with its pager in great detail. L4 has no such interface. It has an extremely simple handler for the physical memory called σ0. This provides no additional paging facility. It is intended to grant all of the available physical pages to a more sophisticated higher-level pager which is referred to as σ1.

I do not see the advantage in placing σ0 outside the kernel. It requires that the kernel pass considerable information about the physical state of the machine to σ0 (though this is achieved in an efficient manner). It is necessary to define an IPC protocol to access σ0 as part of the kernel definition as otherwise the task of writing σ1 would be impossible. The σ0 protocol definition notes that `Special σ0 implementations may extend this protocol' which is unwise in my opinion since it could lead to incompatible implementations.

Conceptually then, σ0 may be considered to be part of the kernel. The only advantage to having σ0 separate to the kernel is that it allows for separate compilation of σ0 which may be convenient in certain situations. The design of σ0 is such that it will not be required after the initial OS bootstrap, except to refuse requests for any further memory allocation. It might lead to a more efficiemt implementation to put σ0 inside the kernel and have a system for removing initialisation code from the kernel as recent Linux kernels do.